$\forall$$B$, $T$:Type, $a$:Knd, ${\it tg}$:Id, $l$:IdLnk, $f$:($B$$\rightarrow$($T$ List)).
\\[0ex]($a$ $=$ rcv($l$,${\it tg}$) $\Rightarrow$ $T$ $=$ $B$) $\Rightarrow$ ma{-}single{-}sends0($B$;$T$;$a$;$l$;${\it tg}$;$f$) $\in$ MsgA